As control systems, scheduling systems, protocols and other real-time systems become increasingly complex, verification of their behavior prior to implementation and/or deployment becomes increasingly desirable. These large systems may be simulated using computer modeling techniques, but the complexity of the systems often precludes suitable simulation. An alternate approach becoming widely popular is that of formal verification.
Formal verification is a method of determining whether a system's constraints are met by the system design. Some formal verification systems, or more specifically, model-checking systems, compare logical definitions of constraints on a system's behavior with logical descriptions of the system to verify that the system's behavior will satisfy those constraints. Some of these checks are safety checks, e.g., determining whether a particular state, usually a failure state or other undesirable state, is reachable. Another example includes liveness checks to verify whether a system will get stuck in a “no-progress” cycle, e.g., verifying that an automaton does not repeatedly visit a state where it checks for received data without visiting a state where it transmits data. The logical description of the system may be used to calculate a set of behavior traces of the system, i.e., a set of all possible system behaviors. Those behavior traces are checked against the behavior specification. There are a variety of tools suitable for such formal verification, including HyTech, available through the University of California at Berkeley, Calif., USA; Kronos, available through Verimag, Gières, France; SPIN, available through Lucent Technologies Inc., Murray Hill, N.J., USA; and PVS, available through SRI International, Menlo Park, Calif., USA.
In practice, a system designer provides a logical definition of constraints on a system's behavior and a logical description of the system to the formal verification system. If the logical definition of the intended behavior implies the logical description of the system, the system is true to the intended behavior. If not, changes are made in the logical models and the system is re-verified. Formal verification is a heavy user of computation time. The complexity of the computations can grow exponentially with the complexity of the system being verified.
For the reasons stated above, and for other reasons stated below that will become apparent to those skilled in the art upon reading and understanding the present specification, there is a need in the art for enhancements to methods for formal verification of system designs.